COMMENT ⊗   VALID 00026 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00003 00002	%elepha[s89,jmc]		Elephant 2000
C00004 00003	\noindent Abstract: Elephant 2000 is a vehicle for some ideas about
C00007 00004	\section{Introduction}
C00019 00005	\section{Speech Acts and Abstract Performatives}
C00024 00006	\section{Referring to the Past}
C00031 00007	\section{The Structure of Elephant 2000 Programs}
C00038 00008	\section{Examples of Programs}
C00044 00009	\section{What is an Airplane Reservation?}
C00047 00010	\section{Additional Features}
C00049 00011	\section{Implementation}
C00062 00012	\section{Verification of Elephant 2000 Programs}
C00063 00013	\section{Relation to Philosophy}
C00073 00014	\section{Algol 50}
C00087 00015	\section{Remarks}
C00088 00016	\section{References}
C00092 00017	\smallskip\centerline{Copyright \copyright\ 1989\ by John McCarthy}
C00093 00018	leftovers
C00095 00019	\section{Speech Acts aka Performatives}
C00102 00020	\noindent Notes:
C00107 00021	\section{Introduction}
C00113 00022	\section{Philosphers' Discussion of Performatives}
C00119 00023	old introduction:
C00125 00024	\subsection{Promises}
C00126 00025	ideas:
C00131 00026	Notes on Searle and Austin
C00133 ENDMK
C⊗;
%elepha[s89,jmc]		Elephant 2000
\input memo.tex[let,jmc]
\centerline{INCOMPLETE PRELIMINARY DRAFT of \jmcdate}
\bigskip
\rightline{\vbox{\it
  \hbox{I meant what I said, and I said what I meant.}
  \hbox{An elephant's faithful, one hundred percent!}
  \smallskip
  \hbox{\rm moreover,}
  \smallskip
  \hbox{An elephant never forgets!}}}
\bigskip
\title{Elephant 2000: A Programming Language Based on Speech Acts}


\medskip
\noindent Abstract: Elephant 2000 is a vehicle for some ideas about
programming language features.
\hfill\break 1. Input and output are in an I-O language whose
sentences are meaningful speech acts approximately in the sense
of philosophers and linguists.  These include questions, answers, offers,
acceptances, declinations,
requests, permissions and promises.
\hfill\break 2. The correctness of programs is partially defined in
terms of proper performance of the speech acts.  Answers should
be truthful, and promises should be kept.  Sentences of logic expressing
these forms of correctness can be generated automatically
from the form of the program.
\hfill\break 3. Elephant source programs may not need data
structures, because they can refer directly to the past.  Thus a
program can say that an airline passenger has a reservation if he
has made one and hasn't cancelled it.
\hfill\break 4. Elephant programs themselves are represented as
sentences of logic.  Their properties follow from this
representation without an intervening theory of programming or
anything like Hoare axioms.
\hfill\break 5. Elephant programs that interact non-trivially with
the outside world can have both {\it illocutionary} and {\it perlocutionary}
specifications, i.e. specifications relating inputs and outputs
and specifications concerning what they do in the world.
\eject
\section{Introduction}

	This paper proposes several new features for programming
languages.  As a vehicle we introduce Elephant 2000, a language
that would embody them.  In the present draft, these features are
not fully embodied in the program examples.

	1. The inputs and outputs to Elephant programs are
sentences of the Elephant I-O language and have meanings
partially determined by the Elephant language and partially
determined in the program itself.  Thus Elephant input and output
includes and the I-O language distinguishes {\it requests}, {\it
questions}, {\it offers}, {\it acceptances of offers}, {\it
permissions} as well as {\it answers to questions} and other
assertions of fact.  Its outputs also include statements of {\it
commitment} analogous to promises.  Some communications between
parts of a program may also be usefully be treated as speech
acts.  This contrasts with present-day programming languages in
which the inputs and outputs are just strings.

	2. Some of the conditions for correctness of an Elephant
program are defined in terms of the meaning of the inputs and
outputs.  We can ask whether an Elephant program understood a
request, fulfilled it, answered a question truthfully, accepted
an offer or fulfilled a commitment. We can also ask whether the
program has authority to do what it does.  We call such
correctness conditions {\it intrinsic}, because the text of the
program determines them.  Expressing these intrinsic correctness
conditions as sentences of logic requires a formal theory of what
it means to fullfil a commitment, etc.  This theory doesn't have
to correspond exactly to human behavior; we only need analogs
useful for program correctness.  The intrinsic correctness sentences
can be generated automatically from the text of the program.

	3. Elephant programs do not require data structures,
because program statements can refer directly to past events and
states.  An Elephant interpreter keeps a history list of past
events, and an Elephant compiler constructs whatever data
structures in the object language are needed to remember the
information needed for compiled program to behave as specified in
the Elephant source program.  It isn't yet clear whether it will be
convenient to omit data structures completely from the language.

	4. An Elephant program is itself a logical sentence
(or perhaps a syntactic sugaring of a logical sentence).  The
correctness properties of the program are logical consequences
of this sentence and a theory of the domain in which the
program acts.  Thus no logic of programs is needed.  Any sugaring
should be reversible by a statement-by-statement syntactic
transformation.

	Elephant programs perform what philosophers and linguists
call {\it speech acts}.  Their idea is that certain sentences
don't have only a declarative significance but are primarily actions,
the paradigm example being a promise, whose utterance creates an
{\it obligation} to fulfill it and is therefore not merely a statement
of intention to do something.  We bypass the philosophical complexities
of the notion of obligation by considering only whether a
particular program does fulfill its obligations.

	Using the customary terminology some of the outputs of
Elephant programs are {\it performative} sentences, commonly
referred to just as {\it performatives}.  Indeed Elephant 2000
started with the idea of making programs use performatives.
However, as the ideas developed, it seemed useful to deviate from
the notions of speech act discussed by J. L. Austin (1955) and
John Searle (1969).  Thinking about speech acts from the {\it
design standpoint} of Daniel Dennett (1971) leads to a view of
them different from the conventional one.  We now refer to {\it
abstract performatives} which include purely internal actions
such as {\it commitments} not necessarily expressed in output,
but on whose fulfillment the correctness of the program depends.
Taking the design stance in the concrete way needed to allow
programs to use speech acts leads to new views on the
philosophical problems that speech acts pose.

	Notice that we don't need to apply moral terms like {\it
honest}, {\it obedient} or {\it faithful} to the program, and we
won't in this paper.  However, we can incorporate as much as we
please of their behavioral meaning in our notions of correctness.

	This article is exploratory, and we are not yet prepared
to argue that every up-to-date programming language of the year
2000 will include {\it abstract performatives}.  We hope that
programs using performatives will be easier to write, understand,
debug and modify.  Having a standard vocabulary of requests,
commitments, etc. will help.  Allowing direct reference to the
past may also permit easier modification, because the program can
refer to past events, e.g. inputs and outputs, directly rather
than via data structures whose design has to be studied and
understood.  Since referring directly to past events is
characteristic of natural languages, we expect it to prove useful
in programming languages.

	The most obvious applications of Elephant are in programs
that do transaction processing and refer to databases in more
general ways than just answering queries and making updates.
Abstract performatives will also be important for programs
involved in business communication with programs belonging
to other organizations as described in (McCarthy 1982).

	5. The theory of speech acts distinguishes between
illocutionary acts, like commanding someone to do something, and
perlocutionary acts, like getting him to do it.  Including
perlocutionary acts in programs is appropriate only if the
program has good enough resources for accomplishing goals to make
it reasonable to put the goal in the program rather than actions
that the programmer believes will achieve it.  One would
therefore expect perlocutionary statements only in programs
exhibiting intelligence.

	However, perlocutionary specifications for a program make
sense.  For example, an air traffic control program may be specified
in terms of the relations between its inputs and its outputs.  This
is an illocutionary specification.  It may also be specified that
it prevents airplanes from colliding, which is a pelocutionary
specification.  Proving that a program meets perlocutionary specifications
must be based on assumptions about the world, the information
it makes available to the program and the effects of the program's
actions.  For this reason, it is worthwhile to formulate both
illocutionary and perlocutionary specifications and to relate them.
For example, an argument based on assumptions about the world may
be used to show that a program meeting certain illocutionary
specifications will also meet certain perlocutionary specifications.

	I considered using the terms {\it internal} and {\it external}
instead of {\it illocutionary} and {\it perlocutionary}, but it seemed
that these gave opportunities for confusion.  Therefore, I'm sticking
to the philosophical jargon even though it involves a considerable
extension of the philosophical usage which applies to single statements.
\section{Speech Acts and Abstract Performatives}

	Philsophers and linguists mostly treat speech acts
naturalistically, i.e. they ask what kinds of speech acts people
perform.  Our approach is to ask what kinds of speech act are
useful in interactive situations.  The nature of the interaction
arises from the fact that the different agents have different
goals, knowledge and capabilities, and an agent's achieving its
goals requires interaction with others.  The nature of the
required interactions determines the speech acts required.  Many
facts about what speech acts are required are independent of
whether the agent is man or machine.

	Often our programs can perform successfully with a small
repertoire of speech acts, and where these speech acts don't have
all the properties John Searle (1969) and other philosophers have
ascribed to human speech acts.

	Here are some of the kinds of speech acts we plan to provide
for.

	1. Assertions.  Correctness requires that the assertions
be truthful.  Of course, proving them true is based on axioms
about the domain in which the program operates.

	2. Questions.  The user can question the program, and the
program can question the user.

	3. Answers to questions.  These are assertions and must
be truthful.  However, they should also be responsive to the
questions.  How to specify this remains to be seen.

	The assertions and questions involve certain predicate
and function symbols common to the user and the program.  These
make up the {\it I-O language} of the program and are to be
combined using the tools of first order logic.  Natural language
front ends might be provided if found helpful.  The I-O language
of a particular program is described in the manual for the
program.  However, certain predicates and functions are common to
all Elephant 2000 programs, whereas many others are close enough to
ordinary language words to be usable without study.

	3. Commitments and promises.  We consider promises as
made up of two parts---the commitment and the statement of the
commitment.  A commitment is a purely internal action by a
program.  Its operand is an act that the program can perform.  A
program is correct only if it fulfills its commitments.

	A promise consists of a commitment to do something, and
an assertion that the commitment exists.  Correctness requires
that the assertion be truthful.

	Commitments in our sense constitute one kind of {\it abstract
performative}; there may be others.  It is abstract in that its
content is independent of how it is expressed, and it need not
be externally expressed at all.
\section{Referring to the Past}

	Algolic programs refer to the past via variables, arrays
and other data structures.  Elephant 2000 programs can refer to
the past directly.  This is not such a great difference, because
it can be regarded as having a single virtual history list or
journal (in I.B.M. language).  It is then a virtual side-effect
of actions to record the action in the history list.  Calling the
history list virtual means that it may not actually take that
form in a compiled program which may use conventional arrays and
not record information that isn't going to be referred to.

	Why allow direct reference to the past?

	1. Humans do it, so it may be convenient.  We'll see.

	2. Most work programmers do is revising programs rather than
writing them {\it ab initio}.  Much of this work involves understanding
the program to be revised.  We would like to be able to revise programs
without reading them, at least reading as little as possible.
If the original programmer designed data structures, it is hardly
going to be possible to revise the program without reading descriptions
of the data structures whose design may require revision.  However,
if memory takes the form of reference to past events, there is a better
chance that the events will not require revision.
The airline reservation programs of this paper give reason to hope
that this strategy will work.

	3. We needn't be fanatical about this.  Elephant 2000 can include
arrays and have actions that stores information in them.  If we regard
storing information in an array as an event, we can have it both ways.

	How should we refer to the past.  Here are some alternatives.

	1. Use temporal modal operators like {\bf P} and {\bf F} to
assert that an event occured in the past or future.  These can be
compounded.  This has been much advocated for proving programs correct,
but it hasn't been used in programming languages themselves.  Anyway
the modal operators seem too weak for our purposes.

	2. Use quantifiers over times.  Here's an example.
%
$$\eqalign{∀psgr flt t(has.&reservation(psgr,flt,t)\cr
≡ ∃t'&(t' < t ∧ made.reservation(psgr,flt,t')\cr
&∧ ∀t''(t' < t'' ∧ t'' < t ⊃ ¬cancelled.reservation(psgr,flt,t'')))).\cr}$$
%
It asserts that a passenger has a reservation if there is a time
at which one was made for him and which was not followed by a
subsequent cancellation.

	I believe that quantification over time is also
insufficiently expressive, and I have two examples that indicate
it.

	2.1. Consider an Elephant 2000 interpreter for a language
that provides for recursive subroutines.  We would like to say
that when a program exits a subroutine, control passes to the
statement after the {\it corresponding} entry to the subroutine.
This involves a structure of ``parentheses'' in the history where
an entry is a left parenthesis and an exit is a right
parenthesis.  We need to identify the left parenthesis
corresponding to a given right parenthesis.  I believe
quantification over sets of times or list structures of times
will work here.

	2.2. Suppose someone is paid by the hour and works a
variable number of intervals during a pay period and that there
is no a priori bound on the number of intervals.  His pay is
proportional to the sum of the lengths of the intervals.  Proving
that the recursive formula for his pay over a pay period is
additive in the pay periods also seems to require quantification
over list structures with times as some of the leaves.

	However, quantificational formulas like the above seem
somewhat awkward, and it may not be obvious how to define an
adequate class of formulas whose members are readily compiled in
code.

	3. Therefore, we have decided tentatively to use another
idea---pattern matching on the history list using tools like those
of LISP macros or of Prolog programs.  Here's a pseudo-Prolog
program for determining whether a passenger has a reservation.
%
$$\eqalign{hasreservation&(Psgr,Flt,Seat,history)\cr
 :- &finalseg(history,X.U),\cr
&ismakrev(X,Psgr,Flt,Seat),\cr
¬ (∃Y)(member(Y,U),cancelsrev(Y,X).\cr}$$
%
Here  $finalseg$ is a predicate asserting that its second argument is
a final segment of the list comprising its first argument.  $X.U$ is
the Lisp $cons$, also used in some Prolog versions.  The quantifier
part is what is most non-standard, but it is in accordance with
(McCarty 1989).
\section{The Structure of Elephant 2000 Programs}

	Elephant 2000 will be described in terms of an
interpreter.  Compiled programs are to have the same input-output
behavior, but the object program uses ordinary data structures
instead of referring directly to the past.

	The main kind of statement is the RESPONSE statement that
tells how the program responds to some kind of input.  Indeed an
important subclass of Elephant program consists entirely of
RESPONSE statements.

	We suppose that only one input reaches the program at a time.
The runtime system is supposed to achieve this.  We also suppose
that inputs not of the required form are rejected, so that the
Elephant program itself doesn't have to say what is done with them.

	The program responds to each input as it is received.
Thus it can be regarded as a stimulus-response machine.  However,
in deciding on a response the program may inspect the entire past
of its previous inputs and responses.
\section{Examples of Programs}

1. Here is an airline reservation program followed by an
explanation of the notations used.  The identifiers in bold face
are defined in the Elephant language; the others are identifiers
of the particular program.

$${\bf if} ¬full flt {\bf then} {\bf accept.request} {\bf commit} admit(psgr,flt)$$
%
This statement says that if the flight is not full the program should
accept a request to commit itself to admit the passenger to the flight.
%
$${\bf answer.query} {\bf committed} admit(psgr,flt)$$
%
The program should answer a query as to whether it is committed to
admit a particular passenger to a particular flight.
%
$${\bf accept.request} {\bf decommit} admit(psgr,flt)$$
%
It should accept a request to cancel a reservation.
%
$$\eqalign{{\bf if} {\bf now} = {\bf time} flt
& ∧ {\bf committed} admit(psgr,flt)\cr
&{\bf then} {\bf accept.request} admit(psgr,flt)\cr}$$
%
If the passenger requests to be admitted to the flight at the time of the
flight, the program should do it.
%
$$full flt ≡ card\{psgr | {\bf committed} admit(psgr,flt)\} = capacity flt$$
%
This is a definition of the flight being full.

${\bf accept.request}$ is an action defined in the Elephant language.
It means to do what is requested.

${\bf commit}$ is an action of the Elephant language.  It means to commit the
program to do its argument in the future.

$admit(psgr,flt)$ means admitting the passenger $psgr$ to the flight
$flt$.  It is a verb of the particular program.

The condition
$full flt$ refers to the particular flight.  A context mechanism
to be explained later makes it possible for the interpreter to take
the unexplained occurrence of $flt$ as referring to the request
that appears later in the statement.

${\bf answer.query}$ is the action of answering a query.

${\bf committed}$ is a predicate that tells whether a certain commitment
exists.  The interpreter must examine the past to determine whether
a commitment has been made.

${\bf decommit}$ is an action cancelling a commitment.

The definition of the predicate $full$ as applied to flights uses
set theoretic notation.

	Here is a variant of the above program using commitments
as objects.  Its advantage is that $make$, $exists$ and $cancel$
can have meanings and be axiomatized independently of the particular
abstract objects being made, tested and destroyed.  The notion
of faithfulness involving the fulfillment of commitments will not
necessarily extend to other abstract entities.

$${\bf if} ¬full flt {\bf then} {\bf accept.request} {\bf make commitment}
 admit(psgr,flt)$$
%
$${\bf answer.query} {\bf exists commitment} admit(psgr,flt)$$
%
$${\bf accept.request} {\bf cancel commitment} admit(psgr,flt)$$
%
$$\eqalign{{\bf if} {\bf now} = {\bf time} flt
& ∧ {\bf exists commitment} admit(psgr,flt)\cr
&{\bf then} {\bf accept.request} admit(psgr,flt)\cr}$$
%
$$full flt ≡ card\{psgr | {\bf exists commitment} admit(psgr,flt)\} = capacity flt$$
%

2. We can describe a minimal program for a control tower at a
military airport.

It receives requests to land.  If the pilot is non-military
it should refuse.  If the pilot is military and there is
no-one landing or taking off let him land.  Otherwise
it should promise permission to land and ask the pilot to wait.  
These are the program's perlocutionary specifications.
Its illocutionary specifications are in terms of inputs
and outputs.  The assumptions relating the perlocutionary
and illocutionary specifications are that pilots obey
and that its observations are correct.
\section{What is an Airplane Reservation?}

	An airplane reservation includes a commitment by the
airline to allow the passenger on the flight unless the
reservation is cancelled or the airline has another reason to let
the passenger on.  It also includes a commitment to pay denied
boarding compensation if the passenger is not allowed on the
plane unless the airline has a reason to do otherwise.  There are
also certain obligations associated with helping the passenger
complete his trip if the flight is cancelled or if an incoming
connecting flight is too late to make the connection.

	However, we don't want to identify the reservation with
the commitment.  Included in the reservation may be other decisions
by the airline that aren't commitments to the passenger who
may not even know about them.

	Someone might say, ``What good is such a commitment
if it can be cancelled at any time by the airline for any reason?''
In fact, such commitments are quite useful compared to not having
them.  The reason is that airlines are not in business to
systematically avoid honoring reservations.
  One might try to define precisely what commitment there is,
but I don't think that's the right idea.  Instead we rely on
nonmonotonic reasoning.  The commitment is valid unless there is
specific reason not to honor it.  This reason could even be local
to a particular airport and maybe to a particular shift supervisor.

	Thus instead of trying to define a reservation precisely,
we regard it as an abstract object.  Airline reservations can be
requested, can be given, can be cancelled, can be honored and can
fail to be honored.

	Searle (1969) treats promises, etc. as ``institutions''
with rules.  Airline reservations should be regarded as
institutions, ephemeral and changeable, to be sure.
\section{Additional Features}

1. Authorization.  We may want to include in the statement of
an Elephant 2000 program statements of what it is authorized to
do.  If we do that, there will be a sentence asserting that
the program does only what it is authorized to do.  This may
include authorizing people and other programs to perform certain
actions.

2. Set theory.  In referring to the past, we propose to allow the
full resources of set theory including the comprehension schema
that allows defining sets in terms of properties.

3. Contexts.  We propose to allow consider each statement as
defining a context in which abbreviated terms can be used.
\section{Implementation}

	We contemplate that Elephant 2000 will have two kinds
of implementation, interpreted and compiled.

	The interpreted implementation has a single simple data
structure---a history list of events.  Inputs will certainly be
included as events.  In principle, this is all that is required.
However, including actions by the program in the history enables
the interpreter to avoid repeating certain computations.  These
actions are both external and internal.  Histories resemble the
``journals'' kept by some transaction systems.

	The interpreter then examines inputs as they come in and
according to the rules decides what to do with each one.  The
present version of Elephant 2000 only provides for certain
requests, etc. and assumes they arrive in order.  The necessary
synchronization is performed by the runtime system outside of the
program itself, and so is the rejection of inputs that don't
match any program statement.

	Matching event patterns to the history of events is done
explicitly each time an input is interpreted.  The actions that
are logged are those that are part of the Elephant 2000 language.

	The interpreter will therefore be somewhat slow, but for
many purposes it will be adequate.

	An Elephant 2000 compiler will translate programs into an
ordinary programming language, e.g.  Commmon Lisp or C.  It would
put data structures in the object program that would permit
reference to these structures in order to decide what to do and
would update the structures according to the action taken.  In a
full translation, there would be no explicit history in the
object program.
\section{Verification of Elephant 2000 Programs}

	One goal is to express the Elephant 2000 programs as
logical sentences.  Their properties would then be logical
consequences of the sentences expressing the program, the axioms
of Elephant 2000 and a theory of the data domains (if any) of the
program.  In this Elephant resembles Algol 50 (McCarthy 1989).
From the sentences expressing the program, we need to be able to
generate the sentences asserting that the program fulfills its
commitments and answers questions honestly.
\section{Relation to Philosophy}

	We discuss philosophical work on speech acts with two objects.
First, we consider what the computer language use of speech
acts can learn from the extensive work by philosophers.  Second,
considering speech acts as we want computers to do them sheds
light on the philosohical problems.  The two aspects of the philosohical
treatments are so interrelated that we discuss them together.
Here are some remarks.

1. Philosophers treat speech acts as natural phenomena to be studied.
However, they don't treat them from the point of view of anthropology
or linguistics.  Instead they study their essential characteristics
in terms of what they accomplish.  This makes their work more relevant
to computer science and artificial intelligence than linguistic or
anthropological work would be.  Unfortunately, they don't seem to
ask questions about what humans need speech acts for.  This would be
even more relevant to us.

2. My view of speech acts is that they are necessary in the {\it common
sense informatic situation} in which people interact with each other
to achieve their goals.  The most important features of this informatic
situation are independent of the fact that we are humans.  Martians or
robots with independent knowledge and goals would also require speech
acts, and many of them would have similar characteristics to human
speech acts.

3. The point of this paper is that speech acts are valuable when we
design computer systems to interact with humans and with each other.

4. However, only some of the characteristics that philosophers have
ascribed to speech acts are valuable for our purposes.  Which ones
they are will depend on the purposes.

5. Besides the speech acts that are common in human society, it is
convenient to invent others.  Indeed human institutions often involve
the invention of speech acts.  An example is the airplane reservation
discussed in this paper.

6. A particular kind of speech act is an entity in an approximate
theory in the sense of (McCarthy 1979).  For this reason attempts
at precise definitions, e.g. of an airplane reservation, are likely
to be beside the point.  Instead we will have nonmonotonic axioms
(McCarthy 1986) that partially characterize them.

7. Regarding speech acts as events of execution of program statements
may be useful for philosophers also.

8. Performatives that are not really speech acts because they don't
result in external output are also useful.  Our main example is the
commitment.  When a program makes a commitment, its correctness
requires the fulfillment of the commitment.

9. A key question we share with philosophers is that of what must
be true in order that a speech act of a given kind be successfully
performed.

10. This paper plays some role in the controversy between John Searle
(1984) and the artificial intelligence community about whether
computers can really believe and know.  A continuation of his previous
line would say that computers can't really promise either.  Perhaps
he will tell us that they can ``weakly promise'' and tell us what that
means.  Our position is that Elephant 2000 programs perform speech acts
as really as do humans.  The difference between what Elephant 2000 programs
do and what some humans to in this respect will be similar to the
differences among humans.

11. It will often be possible to regard a program not written in Elephant
as though it were by regarding its inputs as questions and requests and
its outputs as promises, etc.  This is the Elephant analog of Newell's
logic level or my (1979) ascribing mental qualities to machines.

12. Austin and Searle distinguish {\it illocutionary} from {\it
perlocutionary} speech acts.  An example is that ordering someone
to do something is illocutionary, but getting him to do it is
perlocutionary.  The same sentence may serve as both, but the
conditions for successful perlocutionary acts don't just involve
what the speaker says; the involve its effect on the hearer.
Both philosophers mention difficulties in making the distinction
precise, but for the purposes of Elephant it's easy.

	The correctness conditions for an illocutionary act
involve the state of the program and its inputs and outputs.  The
correctness conditions for a perlocutionary act depends also on
events in the world.  An airline reservation program may
reasonably be specified in terms of the illocutionary acts it
performs, i.e.  by its inputs and outputs, whereas the
correctness of an air traffic control program is essentially
perlocutionary, because stating the full correctness of the
latter involves stating that it prevents the airplanes from
colliding.

	The same program may have two kinds of specifications
and consequently two notions of correctness---illocutionary
and perlocutionary.  The illocutionary specifications of a
program are in terms of its outputs as functions of the
inputs.  The perlocutionary specifications are in terms
of what the program accomplishes in the world.  It may
be useful to give both kinds of specification for the
same program and consider their relations.  Proving that
a program meets its perlocutionary specifications requires
assumptions about the world.  It may be useful to prove for
a given program that if it meets its illocutionary specifications
it will also meet its perlocutionary specifications.  For
example, we would use our assumptions about the behavior
of airplanes and pilots to show that if an air traffic
control program emitted outputs in accordance with its
specifications, then the airplanes wouldn't collide.

	In this connection it may be worthwhile to go beyond
philosophical usage and apply the term {\it perlocutionary} to inputs as
well as outputs.  Namely, perlocutionary conditions on the inputs
state that they give facts about the world, e.g. the locations
of the airplanes.  The correctness of an air traffic control
program depends on assumptions about the correctness of the inputs
as well as on assumptions about the obedience of the pilots and
the physics of airplane flight.
\section{Algol 50}

	We introduce the ``programmng language'' Algol 50 to
illustrate in a simpler setting some ideas that will be wanted in
Elephant 2000.  These are the explicit use of time in a
programming language and the representation of the program by
logical sentences.  The latter permits proofs of properties of
programs without any special theory of programming.  The
properties are deduced from the program itself together with
axioms for the domain.

	The language is called Algol 50, because it covers much
of the ground of Algol 60 but uses only a mathematical formalism,
old fashioned recursion equations, that precedes the development
of programming languages.  It is a programming language I imagine
mathematicians might have created in 1950 had they seen the need
for something other than machine language.

	Consider the Algol 60 fragment.

%$$\eqalign{
%start:\quad &p := 0;\cr
%	&i := n;\cr
%loop: &{\bf if} i=0 {\bf then go to} done;\cr
%	&p := p+m;\cr
%	&i := i-1;\cr
%	&{\bf go to} loop;\cr
%done:\cr}.$$
%
% This is Carolyn's incantation for programs
$$\vtop{\openup\jot\ialign{&$#$\hfil\cr
start:\quad &p := 0;\cr
	&i := n;\cr
loop: &{\bf if} i=0 {\bf then go to} done;\cr
	&p := p+m;\cr
	&i := i-1;\cr
	&{\bf go to} loop;\cr
done:\cr}}.$$

	The program computes the product $mn$ by initializing a
partial product $p$ to zero and then adding $m$ to it $n$ times.
The correctness of the Algol 60 program is represented by the
statement that if the program is entered at $start$ it will reach
the label $done$, and when it does, the variable $p$ will have
the value $mn$.  Different program verification formalisms
represent this assertion in various ways, often not entirely
formal.

	Its partial correctness is conventionally proved by
attaching the invariant assertion $p=m(n-i)$ to the label $loop$.
Its termination is proved by noting that the variable $i$ starts
out with the value $n$ and counts down to 0.  This argument is
formalized in various ways in the different formalisms for
verifying programs.

	In the simplest form of Algol 50 we write this algorithm
as a set of old fashioned recursion equations for three functions
of time, namely $p(t)$, $i(t)$ and $pc(t)$, where the first two
correspond to the variables in the program, and $pc(t)$ tells how
the ``program counter'' changes.  The only ideas that would have been
unconventional in 1950 are the explicit use of a program counter and
the conditional expressions.  We have
%
$$\eqalign{p(t+1) = &{\bf if} pc(t) = 0 {\bf then} 0\cr
&{\bf else if} pc(t) = 3 {\bf then} p(t)+m\cr
&{\bf else} p(t)},$$
%
$$\eqalign{i(t+1) = &{\bf if} pc(t) = 1 {\bf then} n\cr
&{\bf else if} pc(t) = 4 {\bf then} i(t)-1\cr
&{\bf else} i(t)},$$
%
and
%
$$\eqalign{pc(t+1) = &{\bf if} pc(t) = 2 ∧ i(t)= 0 {\bf then} 6 \cr
&{\bf else if} pc(t) = 5 {\bf then} 2 \cr
&{\bf else} pc(t)+1}.$$

	The correctness of the Algol 50 program is represented by
the sentence
%
$$∀n(n≥0 ⊃ ∀t(pc(t) = 0 ⊃ ∃t'(t' > 0 ∧ pc(t') = 6 ∧ p(t') = mn))).$$
%
This sentence may be proved from the sentences representing the
program supplemented by the axioms of arithmetic and the axiom
schema of mathematical induction.  No special theory of programming
is required.  The easiest proof uses mathematical induction on $n$
applied to a formula involving the above-mentioned loop
invariant.

	In the above formalism, Algol 50 programs are organized
quite differently from Algol 60 programs.  Namely, the changes to
variables are sorted by variable rather than sequentially by
time.  However, reifying variables permits rewriting Algol 50
programs in a way that permits regarding programs in this
fragment of Algol 60 as just sugared versions of Algol 50
programs.

	Instead of writing $var(t)$ for some variable $var$, we
write $value(var,\xi(t))$, where $\xi$ is a state vector giving
the values of all the variables.  In the above program, we'll
have $value(p,\xi(t))$, $value(i,\xi(t))$ and $value(pc,\xi(t))$.

	The variables of the Algol 60 program correspond to
functions of time in the above first Algol 50 version and
become distinct constant symbols in the version of Algol
50 with reified variables.
Their distinctness is made explicity by the ``unique names'' axiom

$$i≠p∧i≠pc∧p≠pc.$$

	In expressing the program we use the assignment and
contents functions, $a(var,value,\xi)$ and $c(var,\xi)$, of
(McCarthy 1963) and (McCarthy and Painter 1967).
$a(var,value,\xi)$ is the new state $\xi'$ that results when the
variable $var$ is assigned the value $value$ in state $\xi$.
$c(var,\xi)$ is the value of $var$ in state $\xi$.

	As described in those papers the functions $a$ and $c$
satisfy the axioms.
%
$$c(var,a(var,val,\xi)) = val,$$
%
$$var1 ≠ var2 ⊃ c(var2,a(var1,val,\xi)) = c(var2,\xi),$$
%
$$a(var,val2,a(var,val1,\xi)) = a(var,val2,\xi),$$
%
and
$$var1 ≠ var2 ⊃ a(var2,val2,a(var1,val1,\xi)) = a(var1,val1,a(var2,val2,\xi)).$$

	The following definitions
shorten the expression of programs.

$$step(\xi) = a(pc,value(pc,\xi)+1,\xi),$$
%
$$goto(label,\xi) = a(pc,label,\xi).$$

	We make the further abbreviation $loop = start+2$ specially for this
program, and with this notation our program becomes
%
$$\eqalign{∀t(\xi(t+1) = &{\bf if} c(pc,\xi(t)) = start\cr
&\quad{\bf then} step a(p,0,\xi(t))\cr
&{\bf else if} c(pc,\xi(t)) = start+1\cr
&\quad{\bf then} step a(i,n,\xi(t))\cr
&{\bf else if} c(pc,\xi(t)) = loop\cr
&\quad{\bf then} ({\bf if} c(i,\xi(t)) = 0 {\bf then} goto(done,\xi(t)) {\bf else}
step \xi(t))\cr
&{\bf else if} c(pc,\xi(t)) = loop + 1\cr
&\quad{\bf then} step a(p,c(p,\xi(t))+m,\xi(t))\cr
&{\bf else if} c(pc,\xi(t)) = loop +2\cr
&\quad{\bf then} step a(i,c(i,\xi(t))-1)\cr
&{\bf else if} c(pc,\xi(t)) = loop +3\cr
&\quad{\bf then} goto(loop,\xi(t))\cr
&{\bf else} \xi(t+1))\cr}
$$

	In this form of Algol 50, the consequents of the clauses
of the conditional expression are in 1-1 correspondence with the
statements of the corresponding Algol 60 program.  Therefore, the
Algol 60 program can be regarded as an abbreviation of the
corresponding Algol 50 program.  The (operational) semantics of
the Algol 60 program is then given by the sentence expressing the
corresponding Algol 50 program together with the axioms
describing the data domain, which in this case would be the Peano
axioms for natural numbers.  The transformation to go from Algol
60 to Algol 50 would be entirely local, i.e. statement by
statement, were it not for the need to use statement numbers
explicitly in Algol 50.

	Program fragments can be combined into larger fragments
by taking the conjunction of the sentences representing them,
identifying labels where this is wanted to achieve a {\bf go to}
from one fragment to another and adding sentences to make it
provable that the program counter ranges don't overlap.

	The correctness of this version of the Algol 50 program
is expressed by
%
$$\eqalign{∀t \xi↓0(c(pc,\xi(t))=start& ∧ \xi(t) = \xi↓0\cr
&⊃ ∃t'(t' > t ∧ c(p,xi(t')) = mn\cr
&\quad ∧ c(pc,\xi(t')) = done\cr
&\quad ∧ ∀var(¬(var \in \{p,i\}) ⊃ c(var,\xi(t')) = c(var,\xi↓0))))\cr}$$

	Note that we quantify over all initial state vectors.  The
last part of the correctness formula states that the program fragment
doesn't alter the state vector other than by altering $p$ and $i$.

	We have not carried the Algol 50 idea far enough to
verify that all of Algol 60 is conveniently representable in the same style,
but no fundamental difficulties are apparent.  In treating
recursive procedures, a stack can be introduced, but it would be
more elegant to do without it by explicitly saying that the
return is to the statement after the corresponding procedure call
and variables are restored to their values at the time of the
call.  This requires the ability to parse the past, needed also
for Elephant 2000.

	We advocate an extended Algol 50 for expressing the
semantics of Algol-like programming languages, although our
present purpose was just to use it as an illustration in a
simpler setting of features that Elephant will require.

	Nissim Francez and Amir Pnueli (see references) used an
explicit time for similar purposes.  Unfortunately, they abandoned
it for temporal logic.
\section{Remarks}

Elephant poses many difficulties of formalization.  Here are some.

1. We want to be able to specify that the answer to a query is
responsive.  The simplest example is when we ask for Joe's
telephone number.  An answer $telephone Joe = telephone Joe$
is surely not responsive.  One simple way of making the answer
responsive is to require that it take the form of a sequence
of digits.  However, it isn't obvious how to specify that.
Clearly we must go up to a meta-level if we want to discuss
the required form of an answer.
\section{References}

\noindent {\bf Austin, J. L. (1955)}: {\it How to Do Things with Words},
Harvard University Press 1975.  (The 1955 lectures edited and published after
Austin's death in 1960).

\noindent {\bf Francez, Nissim and Amir Pnueli (1978)}: ``A Proof Method for Cyclic
Programs'', {\it Acta Informatica} 9, 133-157.

\noindent {\bf Francez, Nissim (1976)}: {\it The Analysis of Cyclic Programs}, PhD
Thesis, Weizmann Institute of Science, Rehovot, Israel.

\noindent {\bf Francez, Nissim (1978)}: ``An Application of a Method for
Analysis of Cyclic Programs'', {\it IEEE Transactions on Software
Engineering}, vol. SE-4, No. 5, pp. 371-378, September 1978.

\noindent {\bf McCarthy, John (1963)}: ``Towards a Mathematical Theory of Computation'',
in Proc.  IFIP Congress 62, North-Holland, Amsterdam.

\noindent {\bf McCarthy, John (1967)}:  ``Correctness of a Compiler for Arithmetic
Expresions'' (with James Painter),
{\it Proceedings of Symposia in Applied Mathematics, Volume XIX},
American Mathematical Society.

\noindent {\bf McCarthy, John (1979)}:
``Ascribing Mental Qualities to Machines'' in {\it Philosophical Perspectives 
in Artificial Intelligence}, Ringle, Martin (ed.), Harvester Press, July 1979.

\noindent {\bf McCarthy, John (1982)}: ``Common Business Communication Language'', in
{\it Textverarbeitung und B\"urosysteme}, Albert Endres and J\"urgen Reetz, eds.
R. Oldenbourg Verlag, Munich and Vienna 1982.
%  cbcl[f75,jmc]

\noindent {\bf McCarthy, John (1986)}:
``Applications of Circumscription to Formalizing Common Sense Knowledge''
{\it Artificial Intelligence}, April 1986

\noindent
{\bf Newell, Allen (1981)}: ``The Knowledge Level,'' {\it AI Magazine\/},
Vol. 2, No. 2

\noindent {\bf Searle, John R. (1969)}: {\it Speech Acts}
Cambridge, Eng., Univ. Press.

\noindent{\bf Searle, John R. (1984)}: {\it Minds, Brains, and Science},
Cambridge, Mass. : Harvard University Press, 1984.
\smallskip\centerline{Copyright \copyright\ 1989\ by John McCarthy}
\smallskip\noindent{This draft of ELEPHA[S89,JMC]\ TEXed on \jmcdate\ at \theTime}
%File originated on 10-Jun-89
\vfill\eject\end
leftovers

  Also only parts of the program ``authorized'' to
perform certain actions do so.

	This paper is dedicated to the memory of a recent
insufficiently ambitious talk on Programming Languages of the
Year 2000.  There are two contentions.  First, speech acts
are appropriately understood as parts of procedures rather
than as logical sentences.  Second, abstract speech acts
are useful constructs in more advanced programming languages,
leading to programs with expressiveness closer to that of one
person instructing another.

Should E make or accept offers?

But what about consing up a seat assigment?

%
$$\eqalign{input(t,&request(reservation(flight,date,person)))\cr
&∧ card \{x|is\hbox{-}reservation(x,flight,t)\} < capacity(flight)\cr
⊃ output&(t,promise(reservation(flight,date,person))).\cr}$$
\section{Speech Acts aka Performatives}

	Linguists and philosophers of language have classified
and studied non-declarative sentences.  Linguistic attention is
drawn to some kinds of non-declarative sentences because they
have a different syntax from declarative sentences in the
grammars of natural languages.  These include questions and
imperative sentences.  Others, it has been pointed out, need to
be regarded as semantically (or pragmatically) non-declarative
even though they have declarative grammatical forms.  An example,
is the sentence, ``I now pronounce you man and wife''.  It isn't
just a statement of fact, because uttered by a suitable person
under suitable circumstances creates a state of marriage and
gives the two parties the rights and duties thereof.

	These sentences are sometimes called {\it performatives} or
and sometimes {\it speech acts}, so far as I understand
it, whether they are being studied syntactically or pragmatically.
The performatives include questions, commands, requests, ordinary assertions
promises and others like the above marriage example.  It seems to
me that the marriage example might be called a declarative if
the term hadn't been pre-empted.

	The Gaw of Speech Acts is the Berkeley philosopher
John Searle (19xx).  I don't know if he would approve of
what follows.

	As is usual in science and philosophy, speech acts have
been studied entirely (are there exceptions?) as natural
phenomena which are to be observed and characterized.  {\it What
kinds of speech acts are there, and what are their properties?}
As is common in engineering, mathematics and AI, we ask a
different question.  {\it What good are speech acts, and which
kinds should be designed for what purposes?}  Of course, these
studies will interact.

	Here's the idea.  Suppose we include in a programming
language a notion of {\it performative} and give them a distinguished
syntax that permits compilers, program transformers, and proof-checkers
to recognize the different kinds of performatives and parse their
structures.  We can then give these performatives a certain
``semantics'', where we mean semantics in the sense of programming
language semantics, which often corresponds with what linguists
would call pragmatics.  Once we have introduced this semantics
we get certain ``internal'' notions of correctness.  A
 {\it performatively correct} program answers questions
truthfully, carries out its promises, fulfills its commitments,
 obeys properly
authorized commands, obeys restrictions imposed on
its behavior by commands and by ``speech acts''
analogous to the act of marriage.

	The expected benefit of admitting speech acts in
programming languages or even  basing languages on
speech acts is the same as those claimed for other higher
level language constructs.  The programmer's intention
is more clearly represented in the program, the program
is easier to understand and to modify, and the notion
of its correctness is more definite and readily proved.
We also expect programs to be shorter.

	The present paper introduces two other innovations.
The first seems essential to take proper advantage of
including speech acts, and the second makes the programs
shorter.  In the preliminary version of Elephant 2000, we
will not worry about efficient compilability, or even about
compilability at all.  We concentrate on features that
permit the programmer to express what he wants the program
to do.

\section{Reference to the Past}

	

\section{Remarks}

1. The philosophical notion of speech act regards them as natural
kinds whose nature is to be discovered.  This paper treats speech
acts as something to be invented.  The question is what sorts of
speech acts are useful.  Naturally, contemplating human usage is
helpful in deciding what formalisms to introduce.

\noindent Notes:

How should our performatives differ from those of natural language?

1. Our performatives are abstract.  We define
promises without saying how they are to be expressed.  Later
we may choose one or more concrete representations.

What is a reservation?
	It is a commitment to let the passenger sit in a particular
seat on a particular flight.  Perhaps giving the passenger the
reservation consists of truthfully informing him that the system
has made this commitment.  Not quite.  Giving the passenger the
reservation also includes assuming a legal obligation not to
cancel the reservation except for an allowed reason.
Maybe we can regard assuming the legal obligation as an
internal act, and the external act consists in telling the
passenger truthfully that the obligation has been assumed.
Remember that the passenger will normally not know the exact
obligation that has been assumed.  This is another reason
for keeping the notion of reservation abstract.

request reservation(<flight>,<day>)

2. The program should {\it ask for} the information it needs.

3. People have asked whether Elephant is a programming language
or a form of specification.  It is a programming language in
that a compiler can generate a machine language program
from an Elephant program.  However, Elephant lacks a major
quality of ordinary progamming languages.  There is no longer
any guarantee that the program will function correctly.
This is because the process of compilation involves
nonmonotonic inference on the part of the compiler.
The compiler generates assumptions and the correctness
of the compiled program depends on the assumptions being
true.  The compiler will report the assumptions it made,
and if the user doesn't like them, he can say $maybe(not p)$,
in his next version forcing the compiler to generate code
that takes into account the new possibility.  For example,
the compiler will often assume that necessary information
is present.  If told that it might not be present, it will
generate a program that asks for it.

	One of the ideas that came from trying to invent
Elephant is that the above property may be inevitable in
trying to make programming languages that come closer to
the human ability to describe procedures and to describe
modifications to procedures.

	3. The statements include the resources of set theory,
i.e.  the ability to refer to sets defined by properties.  Sets
of times and events are used often.

We need to provide for committed future actions that are not performed
in response to an input.  They might be performed at a promised
time or they might be started by a request and continue
for a long time.
\section{Introduction}

	The Elephant 2000 programming language involves two main ideas.

	1. The language statements include {\it performatives} like
asking questions, making requests, answering questions, making
promises, making pronouncements that create facts (analogous to a
minister pronouncing two people man and wife) and making internal
commitments.
  Giving a passenger a reservation is a
performative of applied interest.

	Speech acts, otherwise known as performatives, have been
studied by philosophers, (Austin 1955) and (Searle 1969), and by
linguists.  They pointed out that they cannot be regarded as
statements that can be true or false.  Their ``happy'' use
involves various conditions such as sincerity, veracity and
fulfillment.  In our programming use, it makes sense to ask
whether the program answers questions truthfully and carries out
its commitments.  This is an intrinsic notion of correctness, i.e.
it doesn't involve external specifications.  It also makes
programs more modular and easier to understand.

	Naturally, the philosophers' and linguists' conditions for
performatives require revision for programming language purposes.

	2. Expressions of the Elephant 2000 language can refer to
the entire past.  This feature means that data structures need
not be present programs.  For this the program ``parses the
past'', i.e. uses pattern matching on the past to give values to
local variables.
by referring to these structures.

\section{Parsing the Past}

	The present form of this section is even more tentative
than the rest of the paper.

	Part of the objective of Elephant 2000 is to make programs
revisable with as little reading as possible.  Consider the following
analogy.  The boss of the airline can tell his underlings: don't
seat Iranians next to Iraqis; they might fight.  He can give this
order with no knowledge of how the reservation system works.  However,
the underlings will have to understand the system and its data
structures quite thoroughly in order to carry out the order.
Our goal is to make it possible to modify the program without knowing
about its data structures.  This can be done most easily if there
aren't any data structures used in the program itself.  All data
structures, except constant ones, are derived from the past action
of the program.  Therefore, if the program can refer to past events
in a sufficiently powerful way, it doesn't need data structures.

	There are several ways that have been proposed for referring
to the past.  These include temporal modal logic and quantificational
formulas with time as a variable.  The latter is more powerful than
the former, but apparently not powerful enough for all purposes.  The
ability to quantify over finite sets of times or lists of times or
LISP-type data structures including times as leaves seems powerful
enough.

	However, our tentative proposal for Elephant 2000 is to regard
the past somewhat as though it were a string and assign values to
bound variables by pattern matching.

\noindent Mathematical Digression on Matching Patterns to Continuous Objects

	If we consider the past as a function of a real variable
time, then there aren't atomic events.  Therefore, matching the
past requires a generalization of the concepts involved in
matching strings.  However, it may not be much more difficult.  A
non-terminal that can match a sequence can be generalized to a
non-terminal that can match an interval.  Perhaps we need to
distinguish between matching open and closed intervals.
\section{Philosphers' Discussion of Performatives}

Austin, p.163
``To sum up, we may say that the verdictive is an exercise of
judgment, the exercitive is an assertion of influence or
exercising of power, the commissive is an assuming of an
obligation or declaring an intention, the behabitive is
the adopting of an attitude, and the expositive is the
clarifying of reasons, arguments, and communications.''
old introduction:

	This article discusses Elephant 2000, a proposed
programming language for programs that interact with people,
other programs and the physical world.  Transaction processing
including expert systems that process transactions would probably
be the major potential application.  The ideas are incomplete, so
the language may take some time to specify let alone implement.
We employ the concept of {\it speech act} or {\it performative}
statement that has been studied by philosophers and linguists.
However, we modify their notions to suit our purposes.

	The main idea is expressed most directly when we
consider a program's interaction with people.  From the point
of view of the person, he has requests and questions and
in return he expects answers, fulfillment of his requests
or commitments to fulfill them later, and he is prepared
for additional questions which he will answer.   Suppose
the user and the program interact using a terminal on which
both type ASCII strings.  If the program is written in any
of the usual programming languages, it is programmed to use
these strings, but they have no intrinsic meaning.  Only
the programmer has in mind what the strings signify.

	Both the inputs and outputs to Elephant 2000 programs
are meaningful.  Some of this meaning is peculiar to the specific
program, but Elephant itself distinguishes requests, questions, offers,
answers and statements of fact.  Its outputs include these categories
and also statements of commitment analogous to promises.  Thus
when a program issues an airline reservation it is making a qualified
commitment to let the passenger board the airplane.

	Programs that interact with other programs also benefit
from meaningful communication.

	The expected advantage of Elephant 2000 over other
programming languages is that programs will be simpler to write
and that some of the specifications, e.g. that it keep its
promises and answer truthfully are intrinsic.  In this respect
they resemble the syntactic requirement that the program be
grammatical.  Writers, readers and modifiers of programs will
find Elephant programs more intelligible.

	Philosophers, e.g. J. L. Austin (1955) and John Searle (1969)
have studied speech acts.  They point out how speech acts differ from
simple declarative sentences and they classify some of the kinds of
speech acts and characterize their properties.  Some of what they
do is useful to us, but much of it isn't.  I also think that looking
at speech acts from the {\it design standpoint}, (Dennett 1971),
clarifies the philosophical problems.

	These intrinsic notions of correctness of Elephant programs
correspond to Austin's notion of a ``happy'' utterance of a speech
act.  It also corresponds to our slogan that an elephant is faithful,
so we'll call a program faithful if it satisfies the intrinsic notions
of correctness.

	The other main feature of Elephant 2000 is the way it handles
memory.  Instead of expressing the storage and retrieval of information,
Elephant programs refer directly to past events, e.g. inputs and outputs.
The programmer can say that a passenger has a reservation if he has
made one and not cancelled it.  Interpreted Elephant keeps a history
list of past events, while Elephant compilers generate appropriate
data structures so that the object programs can make their decisions
and computations.
general ways than just answering queries and making updates.
\subsection{Promises}

	Searle 

1. {\it Normal input and output conditions obtain.}


ideas:

1. The logical form of Elephant is to be a collection of sentences
of logic.  The properties of the program are to follow from the
program itself, the axioms of the domain and possibly from some
general Elephant axioms.

2. This logical form may consist of addtions to history associated
with each event.  The state associated with a history is what is
true when the events in the history have occurred.  Reduced states
include the information necessary to continue to execute the
program.

3. Here is the distinction between illocutionary and perlocutionary
that we will use---and it's sharp.  Correctness of a program
performing only illocutionary acts is defined in terms of the
programs inputs and outputs and perhaps its internal state.
The correctness of programs performing perlocutionary acts
is defined in terms of the state of the world.

4. We may speak of giving illocutionary specifications and perlocutionary
specifications.  Usually when we give illocutionary specifications,
we have something perlocutionary in mind, but we keep it informal.

5. Include requests for permission and giving permission.

old VAL suggestion, get logic formula corresponding to
correct behavior of a program that commits to set x←1
when user requests the value of x.


	We can compare Elephant with ``programming in English''.  
COBOL translates 1960 understanding of programming into English.
That wasn't hard.  

Sept 13
	VAL suggests

for i = 1 to 10 do read(x);
for j = 10 downto 1 do write (x when i was j)

Also
	n:=0; x:=1;
	for n=1 to 10 do x:=(x when n was n-1)*n

for factorial.

The best example: Read a travel diary and find out when the owner visited
Paris last time.

	while not eof read(year,city);
	write(year when city was Paris)

	RPG suggests that speech acts may refer to the past.

more VAL
The following program reads a string of left and right parentheses
and then points to the last unmatched left parenthesis (I think).

	i:=0; depth:=0;
	repeat
	    i:=i+1;
	    read(x);
	    if x='(' then depth:=depth+1
		     else depth:=depth-1
	until eof;
	write(i when (depth was depth) and not (i was i))

(That is, write the value that i had when depth was the same as now last time).

sep 19
	In order to specify the correctness of the reservation program,
we have to put in a restriction that more people can't be admitted to
an airplane than its capacity allows.  Otherwise, we can prove correct
a program that gives a reservation to anyone who asks and lets everyone
on the airplane.  This seems to involve a formalizaton of ``can''.
How can we avoid having to do this?
Notes on Searle and Austin

25 - Searle credits Austin with perlocutionary.
	``One only refers as part of the performance of an illocutionary
act''.
quote from Frege: ``Nur im Zusammenhang eines Satzes bedeuten die
Worter etwas.''

I don't think we need be bound by this.  For the benefit of our programs
we can create a database of words and longer expressions with the
intent that some of them can have definite references for later use
in sentences, internal and external, without an initial commitment
to any particular sentence.  This database can then be extended
by observations of the program.

Because Searle and other philosophers don't have the notion of
approximate theory, they are excessively conservative about
what is meaningful.  For example, ``Searle's dog'' has a meaning
independent of whether he has one, and a reference if he has exactly
one.